\begin{tabbing}
master{-}antecedent\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Master}$; ${\it Config}$; ${\it Sys}$; $m$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:\{$e$:es{-}E{-}interface(${\it es}$;${\it Master}$)$\mid$ $\uparrow$cmseq?(${\it Master}$($e$))\} . es{-}causl(${\it es}$; ($m$($e$)); $e$))\+
\\[0ex]\& (\=$\forall$\=$e_{1}$:\{$e$:es{-}E{-}interface(${\it es}$;${\it Master}$)$\mid$ $\uparrow$cmseq?(${\it Master}$($e$))\} ,\+\+
\\[0ex]$e_{2}$:\{$e$:es{-}E{-}interface(${\it es}$;${\it Master}$)$\mid$ $\uparrow$cmseq?(${\it Master}$($e$))\} .
\-\\[0ex]es{-}locl(${\it es}$; ($m$($e_{1}$)); ($m$($e_{2}$))) $\Rightarrow$ es{-}causl(${\it es}$; $e_{1}$; $e_{2}$))
\-\\[0ex]\& (\=$\forall$$e$:\{$e$:es{-}E{-}interface(${\it es}$;${\it Master}$)$\mid$ $\uparrow$cmseq?(${\it Master}$($e$))\} .\+
\\[0ex]let \=$c$\= = ${\it Config}$($m$($e$)) in\+\+
\\[0ex]($\uparrow$ccpred?($c$))
\-\\[0ex]\& ccpred{-}id($c$) = cmseq{-}to(${\it Master}$($e$)) $\in$ Id
\\[0ex]\& es{-}loc(${\it es}$; ($m$($e$))) = cmseq{-}from(${\it Master}$($e$)) $\in$ Id
\\[0ex]\& \=$\parallel$cmd{-}history\=\{i:l\}\+\+
\\[0ex](${\it es}$; ${\it Config}$; ${\it Cmd}$; ${\it Sys}$; ($m$($e$)))$\parallel$
\-\\[0ex]=
\\[0ex]cmseq{-}num(${\it Master}$($e$))
\\[0ex]$\in$ $\mathbb{Z}$)
\-\-\-\-
\end{tabbing}